<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
  <meta content="text/html; charset=ISO-8859-1"
 http-equiv="content-type">
  <title>Quick Start</title>
</head>
<body style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);"
 vlink="#ff0000" alink="#000088" link="#0000ff">
<big><big><span style="font-weight: bold;">Quick
Start&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
&nbsp;
&nbsp;
&nbsp;
&nbsp;
&nbsp;&nbsp; </span>(see also: <a href="README.html">README</a>)<span
 style="font-weight: bold;"><br>
<br>
</span></big></big><big><span style="font-weight: bold;"></span></big>CLICK
<a href="#WINDOWS_USERS">WINDOWS</a> or <a
 href="#APPLE_USERS:_In_Mac_OS-X_">APPLE/Mac OS-X</a><br>
<br>
<hr style="width: 100%; height: 2px;"><big style="font-weight: bold;"><span
 style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;
-----------------------------------------------------------------</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;
<big style="font-style: italic; text-decoration: underline;">Quick
Start CHEAT SHEET!!!</big>&nbsp; (see also <a href="README.html">mmj2\README.html</a>)</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;
-----------------------------------------------------------------&nbsp;&nbsp;&nbsp;
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Quick
Start!!!:</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Windows:&nbsp;
Double-click <code>mmj2\mmj2jar\mmj2.bat</code> in
Windows Explorer</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Mac
OS-X: Double-click mmj2\mmj2jar\MacMMJ2.command in Finder</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
BUT...WAIT!...before
running mmj2, edit, if needed:</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
EDIT--&gt;Windows&nbsp;&nbsp;&nbsp;
mmj2\mmj2jar\RunParms.txt</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
using&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
mmj2\mmj2jar\mmj2.bat</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Notepad:&nbsp;&nbsp;
mmj2\mmj2jar\mmj2PATutorial.bat</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
--&gt;Mac
OS-X&nbsp;&nbsp; mmj2\mmj2jar\RunParms.txt</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
using&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
mmj2\mmj2jar\MacRunParmsPATutorial.txt&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
TextEdit:&nbsp;
mmj2\mmj2jar\MacMMJ2.command</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
mmj2\mmj2jar\MacMMJ2PATutorial.command</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
(Double-click
works well now because the new "mmj2 Fail Popup</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Window"
*not only* provides start-up and "fail" error</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
messages,
but it also forces the Windows Command Prompt (Mac</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
OS-X
utilities\terminal.app) window to stay open, which makes</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
it
possible to see all of the mmj2 output about the error.)</span></big><big
 style="font-weight: bold;"><br>
</big>
<hr style="width: 100%; height: 2px;"><br>
<big><span style="font-style: italic;">(Copied fr</span></big><big><span
 style="font-style: italic;">om </span></big><big><span
 style="font-style: italic;">Norm's writing in </span><a
 style="font-style: italic;"
 href="doc/BottomUpProving-ByNormMegill.html">BottomUpProving-ByNormMegill</a><span
 style="font-style: italic;"> and then slightly adjusted):</span></big><br
 style="font-style: italic;">
<br>
<span
 style="font-style: italic; color: rgb(0, 153, 0); font-weight: bold;"><a
 name="WINDOWS_USERS"></a>WINDOWS
USERS:</span><br>
I'll start at the beginning, assuming you are using Windows, so you
won't have to read the mmj2 documentation.&nbsp; Download the latest <code><a
 href="http://us2.metamath.org:8888/index.html#mmj2">mmj2.zip</a></code>
and put it in <code>c:\mmj2.zip</code>.&nbsp; Extract the Zip file to
create <code>c:\mmj2</code> with default settings.&nbsp; From the
result, move or copy the directory <code>c:\mmj2\mmj2jar</code> to <code>c:\mmj2jar</code>
(run <code>c:\mmj2\mmj2jar\copymmj2jar.bat</code> to create and copy <code>c:\mmj2jar</code>
-- see below for instructions on running a "<code>.bat</code>" file.)<br>
<br>
I assume you have Java installed.&nbsp; If not, I guess you'll have to
read the mmj2 documentation after all.<br>
<br>
Next, download <a href="http://us2.metamath.org:8888/metamath/set.mm">set.mm</a>
(6MB) into the directory <code>c:\metamath</code>.&nbsp; Or, if you
want it somewhere else, change the parameter <br>
<br>
<code style="font-weight: bold;">&nbsp; </code><code
 style="font-weight: bold;">LoadFile,set.mm</code><br>
<br>
accordingly, using a text editor like Notepad to edit<br>
<br>
<code style="font-weight: bold;">&nbsp;&nbsp; c:\mmj2jar\RunParms.txt</code><br>
<br>
You may need to update the mmj2Path and MetamathPath arguments in
mmj2.bat (command line arguments #3 and 4 after "<code>mmj2.jar</code>"
-- see <a href="doc/mmj2CommandLineArguments.html">mmj2CommandLineArguments</a>)
in:<br>
<br>
<code style="font-weight: bold;">&nbsp;&nbsp; c:\mmj2jar\mmj2.bat<br>
</code><br>
Then double-click the <code>c:\mmj2jar\mmj2.bat</code> file in Windows
Explorer<br>
<br>
<big><span style="font-weight: bold;">OR</span></big> <br>
<br>
Start a session of Windows Accessories/Command Prompt and enter:<br>
<br>
<code style="font-weight: bold;">&nbsp;&nbsp; cd c:\mmj2jar<br>
</code><br>
Then enter<br>
<br>
<code style="font-weight: bold;">&nbsp;&nbsp; mmj2<br>
</code><br>
<hr style="width: 100%; height: 2px;"><br>
<span
 style="font-style: italic; color: rgb(0, 153, 0); font-weight: bold;"><a
 name="APPLE_USERS:_In_Mac_OS-X_"></a>APPLE
USERS:</span> <big style="text-decoration: underline;"><span
 style="font-weight: bold;">In Mac OS-X</span></big> <br>
<br>
Download the latest <code><a
 href="http://us2.metamath.org:8888/index.html#mmj2">mmj2.zip</a></code>
and put it in <code>/Users/</code><span
 style="font-style: italic; font-weight: bold;">userone</span>&nbsp; --
substituting your directory name for "<span
 style="font-style: italic; font-weight: bold;">userone</span>".<br>
<br>
Extract the Zip file to
create&nbsp;<code>/Users/</code><span
 style="font-style: italic; font-weight: bold;">userone</span><code>/mmj2</code>
with default settings.&nbsp; <br>
<br>
I assume you have Java installed.&nbsp; If not, download it from Apple.
Or Oracle. Follow their instructions.<br>
<br>
Next, download <a href="http://us2.metamath.org:8888/metamath/set.mm">set.mm</a>
(6MB) into the directory&nbsp;<code>/Users/</code><span
 style="font-style: italic; font-weight: bold;">userone</span><code>/</code><code>metamath</code>.&nbsp;
Or,
if
you
want
it
somewhere else, change the parameter <br>
<br>
<code style="font-weight: bold;">&nbsp; </code><code
 style="font-weight: bold;">LoadFile,set.mm</code><br>
<br>
accordingly, using <code style="font-weight: bold;">TextEdit.app</code>
to edit<br>
<br>
<code style="font-weight: bold;">&nbsp;</code><code>
<span style="font-weight: bold;">/Users/</span></code><span
 style="font-style: italic; font-weight: bold;">userone</span><code
 style="font-weight: bold;">/mmj2/mmj2jar/RunParms.txt<br>
</code><br>
You will need to update the mmj2Path and MetamathPath arguments in <a
 href="mmj2jar/MacMMJ2.command"><code style="font-weight: bold;">MacMMJ2.command</code></a>
(command line
arguments #3 and 4 after "<code>mmj2.jar</code>" -- see <a
 href="doc/mmj2CommandLineArguments.html">mmj2CommandLineArguments</a>)
in:<br>
<br>
<code style="font-weight: bold;">&nbsp;</code> <code
 style="font-weight: bold;">/Users/</code><span
 style="font-style: italic; font-weight: bold;">userone</span><code><span
 style="font-weight: bold;">/mmj2/mmj2jar/MacMMJ2.command</span><br>
<br>
&nbsp;</code>and while you're doing this, update this one too:<code><br>
</code><br>
<code style="font-weight: bold;">&nbsp;</code> <code
 style="font-weight: bold;">/Users/</code><span
 style="font-style: italic; font-weight: bold;">userone</span><code><span
 style="font-weight: bold;">/mmj2/mmj2jar/MacPATutorial.command</span><br>
</code><br>
<code><br>
</code>Then&nbsp; double-click the <code>/Users/</code><span
 style="font-style: italic; font-weight: bold;">userone</span><code>/mmj2/mmj2jar/MacMMJ2.command</code>
file in the Finder window<br>
<br>
<br>
<span style="font-style: italic;"></span>
<hr style="width: 100%; height: 2px;"><br>
</body>
</html>
